EventsWithState
== E:Type
==  (eq:EqDecider(E)
==  pred?:(E(?E))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms(E; pred?; info)
==  T:(IdIdType)
==  V:(IdIdType)
==  M:(IdLnkIdType)
==  init:(i:IdEState(T(i)))
==  Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )EState(T(i))EState(T(i)))
==  val:(e:Ekindcase(kind(e); a.V(loc(e),a); l,t.M(l,t) ))
==  Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List))
==  Choose:(i,a:Id(x:IdT(i,x))(?(V(i,a))))
==  time:(E)
==  (va:val-axiom(E;V;M;info;pred?;
==  (va:init;Trans;
==  (va:Choose;Send;val;time)
==  Top)) 

latex

---

clarification:

E-State{i:l}
== E:Type{i}
==  (eq:EqDecider(E)
==  pred?:(E(E + Unit))
==  info:(E((:Id  Id) + (:(:IdLnk  E)  Id)))
==  oaxioms:EOrderAxioms{i}(E;
==  oaxioms:EOpred?;
==  oaxioms:EOinfo)
==  T:(IdIdType{i})
==  V:(IdIdType{i})
==  M:(IdLnkIdType{i})
==  init:(i:IdEState(T(i)))
==  Trans:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )EState(T(i))EState(T(i)))
==  val:(e:Ekindcase(kind(info;e); a.V(loc(info;e),a); l,t.M(l,t) ))
==  Send:(i:Idk:Kndkindcase(k; a.V(i,a); l,t.M(l,t) )(x:IdT(i,x))(Msg(M) List))
==  Choose:(i:Ida:Id(x:IdT(i,x))((V(i,a)) + Unit))
==  time:(E)
==  (va:val-axiom(E;V;M;info;pred?;
==  (va:init;Trans;
==  (va:Choose;Send;val;time)
==  Top)) 

latex

Definitions	EqDecider(T), EOrderAxioms(E; pred?; info), IdLnk, Type, EState(T), kind(e), loc(e), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), type List, Msg(M), , Id, left + right, f(a), Unit, x:AB(x), , x:A  B(x), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), Top
FDL editor aliases	EState